;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Ihelpers.lisp")
(require "Mhelpers.lisp")

(module Thelpers
  (import Ihelpers)
  
; check-expect tests  
  (include-book "testing" :dir :teachpacks)
  (check-expect (chrs-words->strings nil) nil)
  (check-expect (chrs-words->strings (list '(#\H #\a #\v #\e) 
                                           '(#\a) '(#\g #\r #\e #\a #\t) 
                                           '(#\d #\a #\y))) (list "Have" "a" "great" "day"))  
  (check-expect (sum-list nil) 0)
  (check-expect (sum-list (list 1 2 3)) 6)
  (check-expect (sum-list (list 1.5 -2.5 3.5)) 2.5)  
  (check-expect (average-list nil) nil)
  (check-expect (average-list (list 1 2 6)) 3)
  (check-expect (average-list (list 1.5 -2.5 7.0)) 2.0)
  (check-expect (get-max nil '("abc" 321)) '("abc" 321))
  (check-expect (get-max (list '("abc" 321) '("def" 456) '("cde" 123)) '("bcd" 231)) '("def" 456))
  (check-expect (get-max (list '("abc" 321) '("bcd" 231) '("cde" 123)) '("def" 456)) '("def" 456))
  
;property definitions
  (include-book "doublecheck" :dir :teachpacks)
  
  (defproperty chrs-words->strings-returns-list-prp
    (words  :value (random-list-of (random-list-of (random-char))))
    (equal t (string-listp (chrs-words->strings words))))
  
  (defproperty sum-list-returns-number-prp
    (numbers  :value (random-list-of (random-rational)))
    (equal t (rationalp (sum-list numbers))))
  
  (defproperty average-list-returns-number-prp
    (numbers  :value (random-list-of (random-rational))
              :where (> (len numbers) 0))
    (equal t (rationalp (average-list numbers))))
  
  (defproperty get-max-returns-stock-data-prp
    (stocks  :value (random-list-of (list (random-string) (random-natural)))
     currmax :value (list (random-string) (random-natural)))
    (equal t (and (stringp (car (get-max stocks currmax))) 
                  (natp (cadr (get-max stocks currmax))))))
  )

(link RThelpers (Mhelpers Thelpers))
(invoke RThelpers)